home *** CD-ROM | disk | FTP | other *** search
/ Amiga Plus Leser 15 / Amiga Plus Leser CD 15.iso / Tools / Development / yacas_alg / yacas_morphos / share / yacas / logic.rep / code.ys < prev   
Encoding:
Text File  |  2002-03-13  |  14.0 KB  |  375 lines
  1. /* Tests on logic */
  2.  
  3. /* Small theorem prover for propositional logic, based on the
  4.  * resolution principle.
  5.  * Written by Ayal Pinkus
  6.  * Version 0.1 initial implementation.
  7.  *
  8.  *
  9.  * Examples:
  10. CanProve(( (a=>b) And (b=>c)=>(a=>c) ))  <-- True
  11. CanProve(a  Or   Not a)                  <-- True
  12. CanProve(True  Or  a)                    <-- True
  13. CanProve(False  Or  a)                   <-- a
  14. CanProve(a  And   Not a)                 <-- False
  15. CanProve(a  Or b Or (a And b))           <-- a Or b
  16.  */
  17.  
  18. RuleBase("=>",{a,b});
  19.  
  20.  
  21. /*
  22.    Simplify a boolean expression. CNF is responsible
  23.    for converting an expression to the following form:
  24.         (p1  Or  p2  Or  ...)  And  (q1  Or  q2  Or  ...)  And ...
  25.    That is, a conjunction of disjunctions.
  26. */
  27.  
  28.  
  29. // Trivial simplifications
  30. 10  # CNF( Not  True)                  <-- False;
  31. 11  # CNF( Not  False)                 <-- True;
  32. 12  # CNF(True   And  (_x))            <-- CNF(x);
  33. 13  # CNF(False  And  (_x))            <-- False;
  34. 14  # CNF(_x   And  True)              <-- CNF(x);
  35. 15  # CNF(_x  And  False)              <-- False;
  36. 16  # CNF(True   Or  (_x))             <-- True;
  37. 17  # CNF(False  Or  (_x))             <-- CNF(x);
  38. 18  # CNF((_x)  Or  True )             <-- True;
  39. 19  # CNF((_x)  Or  False)             <-- CNF(x);
  40.  
  41. // A bit more complext
  42. 21  # CNF(_x  Or  _x)                  <-- CNF(x);
  43. 22  # CNF(_x  And  _x)                 <-- CNF(x);
  44. 23  # CNF(_x  Or Not (_x))             <-- True;
  45. 14  # CNF(Not (_x)  Or _x)             <-- True;
  46. 25  # CNF(_x  And Not (_x))            <-- False;
  47. 26  # CNF(Not (_x)  And _x)            <-- False;
  48.  
  49. // Simplifications that deal with (in)equalities
  50. 25  # CNF(((_x) == (_y))   Or  ((_x) !== (_y)))   <-- True;
  51. 25  # CNF(((_x) !== (_y))  Or  ((_x) == (_y)))    <-- True;
  52. 26  # CNF(((_x) == (_y))   And ((_x) !== (_y)))   <-- False;
  53. 26  # CNF(((_x) !== (_y))  And ((_x) == (_y)))    <-- False;
  54.  
  55. 27  # CNF(((_x) >= (_y))   And ((_x) < (_y)))     <-- False;
  56. 27  # CNF(((_x) < (_y))    And ((_x) >= (_y)))    <-- False;
  57. 28  # CNF(((_x) >= (_y))   Or  ((_x) < (_y)))     <-- True;
  58. 28  # CNF(((_x) < (_y))    Or  ((_x) >= (_y)))    <-- True;
  59.  
  60. // some things that are more complex
  61. 120  # CNF((_x)  Or  (_y))            <-- LogOr(x, y, CNF(x), CNF(y));
  62. 10 # LogOr(_x,_y,_x,_y)               <-- x Or y;
  63. 20 # LogOr(_x,_y,_u,_v)               <-- CNF(u Or v);
  64.  
  65. 130  # CNF( Not  (_x))                <-- LogNot(x, CNF(x));
  66. 10 # LogNot(_x, _x)                   <-- Not (x);
  67. 20 # LogNot(_x, _y)                   <-- CNF(Not (y));
  68.  
  69. 40 # CNF( Not ( Not  (_x)))           <-- CNF(x);                           // eliminate double negation
  70. 45 # CNF((_x)=>(_y))                  <-- CNF((Not (x))  Or  (y));              // eliminate implication
  71.  
  72. 50 # CNF( Not ((_x)  And  (_y)))      <-- CNF((Not x) Or (Not y));          // De Morgan's law
  73. 60 # CNF( Not ((_x)  Or  (_y)))       <-- CNF(Not (x)) And CNF(Not (y));        // De Morgan's law
  74.  
  75. /*
  76. 70 # CNF((_x) And ((_y)  Or  (_z)))   <-- CNF(x And y) Or CNF(x And z);
  77. 70 # CNF(((_x) Or (_y)) And (_z))     <-- CNF(x And z) Or CNF(y And z);
  78.  
  79. 80 # CNF((_x)  Or  ((_y)  And  (_z))) <-- CNF(x Or y) And CNF(x Or z);
  80. 80 # CNF(((_x)  And  (_y)) Or (_z))   <-- CNF(x Or z) And CNF(y Or z);
  81. */
  82.  
  83. 70 # CNF(((_x)  And  (_y))  Or  (_z)) <-- CNF(x Or z) And CNF(y Or z);      // Distributing Or over And
  84. 80 # CNF((_x)  Or  ((_y)  And  (_z))) <-- CNF(x Or y) And CNF(x Or z);
  85.  
  86. 90 # CNF((_x)  And  (_y))             <-- CNF(x) And CNF(y);                // Transform subexpression
  87.  
  88. 101 # CNF( (_x) < (_y) )              <-- Not CNFInEq(x >=  y);
  89. 102 # CNF( (_x) > (_y) )              <-- CNFInEq(x >   y);
  90. 103 # CNF( (_x) >= (_y) )             <-- CNFInEq(x >=  y);
  91. 104 # CNF( (_x) <= (_y) )             <-- Not CNFInEq(x >  y);
  92. 105 # CNF( (_x) == (_y) )             <-- CNFInEq(x ==  y);
  93. 106 # CNF( (_x) !== (_y) )            <-- Not CNFInEq(x == y);
  94.  
  95. 111 # CNF( Not((_x) <  (_y)) )        <-- CNFInEq( x >= y );
  96. 113 # CNF( Not((_x) <= (_y)) )        <-- CNFInEq( x > y );
  97. 116 # CNF( Not((_x) !== (_y)) )       <-- CNFInEq( x == y );
  98.  
  99. /* Accept as fully simplified, fallthrough case */
  100. 200 # CNF(_x)                         <-- x;
  101.  
  102. 20 # CNFInEq((_xex) == (_yex))        <-- (CNFInEqSimplify(xex-yex) ==  0);
  103. 20 # CNFInEq((_xex) > (_yex))         <-- (CNFInEqSimplify(xex-yex) >   0);
  104. 20 # CNFInEq((_xex) >= (_yex))        <-- (CNFInEqSimplify(xex-yex) >=  0);
  105. 30 # CNFInEq(_exp)                    <-- (CNFInEqSimplify(exp));
  106.  
  107. 10 # CNFInEqSimplify((_x) - (_x))     <-- 0;        // strictly speaking, this is not always valid, i.e. 1/0 - 1/0 != 0...
  108. 100# CNFInEqSimplify(_x)              <-- [/*Echo({"Hit the bottom of CNFInEqSimplify with ", x, Nl()});*/ x;];
  109.                                                     // former "Simplify";
  110.  
  111. // Some shortcuts to match prev interface
  112. CanProveAux(_proposition)                           <-- LogicSimplify(proposition, 3);
  113. 10 # LogicSimplify(_proposition, _level)_(level<2)  <-- CNF(proposition);
  114.  
  115. 20 # LogicSimplify(_proposition, _level) <--
  116. [
  117.   Local(cnf, list, clauses);
  118.   Check(level > 1, "Wrong level");
  119.   // First get the CNF version of the proposition
  120.   Set(cnf, CNF(proposition));
  121.  
  122.   If(level <= 1, cnf, [
  123.     Set(list, Flatten(cnf, "And"));
  124.     Set(clauses, {});
  125.     ForEach(clause, list)
  126.     [
  127.       Local(newclause);
  128.       //newclause := BubbleSort(LogicRemoveTautologies(Flatten(clause, "Or")), LessThan);
  129.       Set(newclause, LogicRemoveTautologies(Flatten(clause, "Or")));
  130.       If(newclause != {True}, DestructiveAppend(clauses, newclause));
  131.     ];
  132.  
  133.     /*
  134.         Note that we sort each of the clauses so that they look the same,
  135.         i.e. if we have (A And B) And ( B And A), only the first one will
  136.         persist.
  137.     */
  138.     Set(clauses, RemoveDuplicates(clauses));
  139.  
  140.     If(Equals(level, 3) And (Length(clauses) != 0), [
  141.         Set(clauses, DoUnitSubsumptionAndResolution(clauses));
  142.         Set(clauses, LogicCombine(clauses));
  143.     ]);
  144.  
  145.     Set(clauses, RemoveDuplicates(clauses));
  146.  
  147.     If(Equals(Length(clauses), 0), True, [
  148.         /* assemble the result back into a boolean expression */
  149.         Local(result);
  150.         Set(result, True);
  151.         ForEach(item,clauses)
  152.         [
  153.             Set(result, result And UnFlatten(item, "Or", False));
  154.         ];
  155.  
  156.         result;
  157.     ]);
  158.   ]);
  159. ];
  160.  
  161. /* CanProve tries to prove that the negation of the negation of
  162.    the proposition is true. Negating twice is just a trick to
  163.    allow all the simplification rules a la De Morgan to operate
  164.  */
  165. /*CanProve(_proposition)    <-- CanProveAux( Not CanProveAux( Not proposition));*/
  166.  
  167. CanProve(_proposition)      <-- CanProveAux( proposition );
  168.  
  169. 1 # SimpleNegate(Not (_x))  <-- x;
  170. 2 # SimpleNegate(_x)        <-- Not(x);
  171.  
  172. /* LogicRemoveTautologies scans a list representing e1 Or e2 Or ... to find
  173.    if there are elements p and  Not p in the list. This signifies p Or Not p,
  174.    which is always True. These pairs are removed. Another function that is used
  175.    is RemoveDuplicates, which converts p Or p into p.
  176. */
  177.  
  178. /* this can be optimized to walk through the lists a bit more efficiently and also take
  179. care of duplicates in one pass */
  180. LocalCmp(_e1, _e2)                  <-- LessThan(ToString() Write(e1), ToString() Write(e2));
  181.  
  182. // we may want to add other expression simplifers for new expression types
  183. 100 # SimplifyExpression(_x)        <-- x;
  184.  
  185. // Return values:
  186. //  {True} means True
  187. //  {} means False
  188. LogicRemoveTautologies(_e) <--
  189. [
  190.   Local(i, len, negationfound); Set(len, Length(e));
  191.   Set(negationfound, False);
  192.  
  193.   //Echo(e);
  194.   e := BubbleSort(e, "LocalCmp");
  195.  
  196.   For(Set(i, 1), (i <= len) And (Not negationfound), i++)
  197.   [
  198.     Local(x, n, j);
  199.     // we can register other simplification rules for expressions
  200.     //e[i] := MathNth(e,i) /:: {gamma(_y) <- SimplifyExpression(gamma(y))};
  201.     Set(x, MathNth(e,i));
  202.     Set(n, SimpleNegate(x));                    /* this is all we have to do because of
  203.                                                 the kind of expressions we can have coming in */
  204.  
  205.     For(Set(j, i+1), (j <= len) And (Not negationfound), j++) [
  206.         Local(y);
  207.         Set(y, MathNth(e,j));
  208.  
  209.         If(Equals(y, n),
  210.             [
  211.                 //Echo({"Deleting from ", e, " i=", i, ", j=", j, Nl()});
  212.  
  213.                 Set(negationfound, True);
  214.                 //Echo({"Removing clause ", i, Nl()});
  215.             ],
  216.         If(Equals(y, x),
  217.             [
  218.                 //Echo({"Deleting from ", e, " j=", j, Nl()});
  219.                 DestructiveDelete(e, j);
  220.                 Set(len,MathSubtract(len,1));
  221.             ])
  222.         );
  223.     ];
  224.     Check(len = Length(e), "The length computation is incorrect");
  225.   ];
  226.  
  227.   If(negationfound, {True}, e);            /* note that a list is returned */
  228. ];
  229.  
  230. 10 # Contradict((_x) - (_y) == 0, (_x) - (_z) == 0)_(y != z)     <-- True;
  231. 12 # Contradict((_x) == (_y), (_x) == (_z))_(y != z)             <-- True;
  232. 13 # Contradict((_x) - (_y) == 0, (_x) - (_z) >= 0)_(z > y)      <-- True;
  233. 14 # Contradict((_x) - (_y) == 0, (_x) - (_z) >  0)_(z > y)      <-- True;
  234. 14 # Contradict(Not (_x) - (_y) >= 0, (_x) - (_z) >  0)_(z > y)  <-- True;
  235. 15 # Contradict(_a, _b)                                          <-- Equals(SimpleNegate(a), b);
  236.  
  237. /* find the number of the list that contains n in it, a pointer to a list of lists in passed */
  238. LogicFindWith(_list, _i, _n) <--
  239. [
  240.   Local(result, index, j);
  241.   Set(result, -1); Set(index, -1);
  242.  
  243.   For(j := i+1, (result<0) And (j <= Length(list)), j++)
  244.   [
  245.     Local(k, len); Set(len, Length(list[j]));
  246.     For(k := 1, (result<0) And (k<=len), k++)
  247.     [
  248.       Local(el); Set(el, list[j][k]);
  249.  
  250.       If(Contradict(n, el),
  251.         [Set(result, j); Set(index, k);]);
  252.     ];
  253.   ];
  254.   {result, index};
  255. ];
  256.  
  257. /* LogicCombine is responsible for scanning a list of lists, which represent
  258.    a form (p1  Or  p2  Or  ...)  And  (q1  Or  q2  Or  ...)  And ... by scanning the lists
  259.    for combinations x Or Y  And   Not x Or Z <-- Y Or Z . If Y Or Z is empty then this clause
  260.    is false, and thus the entire proposition is false.
  261. */
  262. LogicCombine(_list) <--
  263. [
  264.   Local(i, j);
  265.   For(Set(i,1), i<=Length(list), Set(i,MathAdd(i,1)))
  266.   [
  267.     //Echo({"list[", i, "/", Length(list), "]: ", list[i], Nl()});
  268.     Local(redo);
  269.     Set(redo, False);
  270.  
  271.     For(j := 1, Not(redo) And (j<=Length(list[i])), j++)
  272.     [
  273.       Local(tocombine, n, k);
  274.       Set(n, list[i][j]);
  275.  
  276.       {tocombine, k} := LogicFindWith(list, i, n);// search forward for n, tocombine is the list we
  277.                                                   // will combine the current one with
  278.       If(tocombine != -1,
  279.       [
  280.         Local(combination);
  281.         Check(k != -1, "k is -1");
  282.  
  283.         DestructiveDelete(list[i], j);
  284.         DestructiveDelete(list[tocombine], k);
  285.  
  286.         Set(combination, LogicRemoveTautologies(Concat(list[i], list[tocombine])));
  287.         DestructiveDelete(list, tocombine);       // delete tocombine from the list, it's represented
  288.                                                   // by combination, which will be list[i]
  289.         DestructiveReplace(list, i, combination);
  290.  
  291.         If(combination = {False},                 // false is represented as {}
  292.             DestructiveReplace(list, i, combination));
  293.  
  294.         If(combination = {},                      // the combined clause is false, so the whole thing is false
  295.           [Set(list, {{}}); Set(i, Length(list)+1);], [Set(i, 0);]);
  296.  
  297.         Set(redo, True);                          // this signals that we should break out of the inner loop
  298.       ]);
  299.     ];
  300.   ];
  301.   list;
  302. ];
  303.  
  304. 10 # Subsumes((_x) - (_y) == 0, Not ((_x) - (_z)==0))_(y!=z)    <-- True;
  305. // suif_tmp0_127_1-72==0 And 78-suif_tmp0_127_1>=0
  306. 20 # Subsumes((_x) - (_y) == 0, (_z) - (_x) >= 0)_(z>=y)        <-- True;
  307. 20 # Subsumes((_x) - (_y) == 0, (_z) - (_x) >  0)_(z>y)         <-- True;
  308. // suif_tmp0_127_1-72==0 And suif_tmp0_127_1-63>=0
  309. 30 # Subsumes((_x) - (_y) == 0, (_x) - (_z) >= 0)_(y>=z)        <-- True;
  310. 30 # Subsumes((_x) - (_y) == 0, (_x) - (_z) > 0)_(y>z)          <-- True;
  311.  
  312. 90 # Subsumes((_x), (_x))                                       <-- True;
  313.  
  314. 100# Subsumes((_x), (_y))                                       <-- False;
  315.  
  316.  
  317. // perform unit subsumption and resolutiuon for a unit clause # i
  318. // a boolean indicated whether there was a change is returned
  319. DoUnitSubsumptionAndResolution(_list) <--
  320. [
  321.     Local(i, isFalse, isTrue, changed);
  322.     Set(isFalse, False);
  323.     Set(isTrue,  False);
  324.     Set(changed, True);
  325.  
  326.     //Echo({"In DoUnitSubsumptionAndResolution", Nl()});
  327.  
  328.     While(changed) [
  329.       Set(changed, False);
  330.  
  331.       For(i:=1, (Not isFalse And Not isTrue) And i <= Length(list), i++)
  332.       [
  333.         If(Length(list[i]) = 1, [
  334.           Local(x); Set(x, list[i][1]); //n := SimpleNegate(x);
  335.           //Echo({"Unit clause ", x, Nl()});
  336.  
  337.           // found a unit clause, {x}, not use it to modify other clauses
  338.           For(j:=1, (Not isFalse And Not isTrue) And j <= Length(list), j++)
  339.           [
  340.               If(i !=j, [
  341.                 Local(deletedClause); Set(deletedClause, False);
  342.                 For(k:=1, (Not isFalse And Not isTrue And Not deletedClause) And k <= Length(list[j]),  k++)
  343.                 [
  344.                     // In both of these, if a clause becomes empty, the whole thing is False
  345.  
  346.                     //Echo({"   ", x, " subsumes ", list[j][k], i,j, Subsumes(x, list[j][k]), Nl()});
  347.  
  348.                     // unit subsumption -- this kills clause j
  349.                     If(Subsumes(x, list[j][k]), [
  350.                         // delete this clause
  351.                         DestructiveDelete(list, j);
  352.                         j--;
  353.                         If(i>j, i--);   // i also needs to be decremented
  354.                         Set(deletedClause, True);
  355.                         Set(changed, True);
  356.                         If(Length(list) = 0, [Set(isTrue, True);]);
  357.                     ],
  358.                       // else, try unit resolution
  359.                     If(Contradict(x, list[j][k]), [
  360.                         //Echo({x, " contradicts", list[j][k], Nl()});
  361.                         DestructiveDelete(list[j], k);
  362.                         k--;
  363.                         Set(changed, True);
  364.                         If(Length(list[j]) = 0, [Set(isFalse, True);]);
  365.                     ])
  366.                     );
  367.                 ];
  368.               ]);
  369.           ];
  370.         ]);
  371.       ];
  372.     ];
  373.  
  374.     list;
  375. ];